ePMC

Benchmark
Model:wlan v.1 (MDP)
Parameter(s)MAX_BACKOFF = 4, COL = 0
Property:cost_min (exp-reward)
Invocation (default)
java -Xms10240m -Xmx10240m -jar ../epmc-standard.jar check --model-input-files wlan.4.prism --model-input-type prism --property-input-files wlan.props --property-input-names cost_min --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6 --const COL=0
Execution
Walltime:53.46545076370239s
Return code:0
Relative Error:0.0
Log
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property cost_min
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-states-explored 16922 16922
build-model-states-explored 38436 21514
build-model-states-explored 58495 20059
build-model-states-explored 80888 22393
build-model-states-explored 108434 27546
build-model-states-explored 132459 24025
build-model-states-explored 158887 26428
build-model-states-explored 184982 26094
build-model-states-explored 210502 25520
build-model-states-explored 238817 28316
build-model-states-explored 267152 28335
build-model-states-explored 295673 28521
build-model-states-explored 324462 28789
build-model-done 345000 13
iterating
iterating-progress-unbounded 302 0.12578616352201258 1
iterating-done 558 1
model-checking-done 52
command-check-result-is 7625.0 cost_min